Double Categories in Univalent Foundations

Abstract: This is joint work with Niels van der Weide, Benedikt Ahrens and Paige Randall North. In category theory, we typically study categories either up to isomorphisms (considering objects up to equality) or equivalences (considering objects up to isomorphism). Fortunately, since equivalences generalize isomorphisms, this distinction rarely causes mathematical difficulties. However, double categories present a richer structure with multiple notions of equivalence—such as isomorphisms, horizontal equivalences, and gregarious equivalences—none of which subsumes all the others. This creates potential ambiguities, making it necessary to specify the appropriate form of equivalence in any given context. In this talk, I will show how moving from a set-theoretic foundation to a univalent foundation allows for definitions of (double) categories that inherently include the desired notion of equivalence.

category theory

Audience: researchers in the topic

( video )

Second Virtual Workshop on Double Categories